(declare-fun a () (_ BitVec 32))
(push)
(assert (distinct a (_ bv0 32)))
(check-sat)
(pop)
(check-sat)
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))
(declare-fun d () (_ BitVec 32))
(assert (distinct (_ bv0 32) (_ bv1 32)))
(assert (distinct (bvadd d c) (_ bv1 32)))
(assert (= (bvadd (bvmul (_ bv2 32) b) c) (bvadd (bvneg d) (_ bv1 32))))
(check-sat)
